Termination proof of /tmp/tmp3GSN_B/Ex9

Termination of the following Term Rewriting System could not be shown:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(a, b, X) → f(X, X, X)
c → a
c → b

The replacement map contains the following entries:

f: {1, 3}
a: empty set
b: empty set
c: empty set

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Context-sensitive rewrite system:
The TRS R consists of the following rules:

f(a, b, X) → f(X, X, X)
c → a
c → b

The replacement map contains the following entries:

f: {1, 3}
a: empty set
b: empty set
c: empty set

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ ConvertedToQDPProblemProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
For all symbols f in {f, F} we have µ(f) = {1, 3}.

The ordinary context-sensitive dependency pairs DP_o are:

F(a, b, X) → F(X, X, X)

The TRS R consists of the following rules:

f(a, b, X) → f(X, X, X)
c → a
c → b

Q is empty.

Converted QDP Problem, but could not keep Q or minimality.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ ConvertedToQDPProblemProof

        ↳ QDP

          ↳ NonTerminationProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

F(a, b, X) → F(X, X, X)

The TRS R consists of the following rules:

f(a, b, X) → f(X, X, X)
c → a
c → b

Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

F(a, b, X) → F(X, X, X)

The TRS R consists of the following rules:

f(a, b, X) → f(X, X, X)
c → a
c → b

s = F(c, c, X) evaluates to t =F(X, X, X)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [X / c]
Matcher: [ ]

Rewriting sequence

F(c, c, c) → F(c, b, c)
with rule c → b at position [1] and matcher [ ]

F(c, b, c) → F(a, b, c)
with rule c → a at position [0] and matcher [ ]

F(a, b, c) → F(c, c, c)
with rule F(a, b, X) → F(X, X, X)

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

We applied the Incomplete Giesl Middeldorp transformation [11] to transform the context-sensitive TRS to a usual TRS.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

  ↳ Trivial-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(mark(x1), x2, mark(x3))
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(c) → cActive
cActive → c
mark(a) → a
mark(b) → b
fActive(a, b, X) → fActive(mark(X), X, mark(X))
cActive → a
cActive → b

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MARK(f(x1, x2, x3)) → MARK(x3)
MARK(f(x1, x2, x3)) → FACTIVE(mark(x1), x2, mark(x3))
FACTIVE(a, b, X) → FACTIVE(mark(X), X, mark(X))
MARK(f(x1, x2, x3)) → MARK(x1)
FACTIVE(a, b, X) → MARK(X)
MARK(c) → CACTIVE

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(mark(x1), x2, mark(x3))
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(c) → cActive
cActive → c
mark(a) → a
mark(b) → b
fActive(a, b, X) → fActive(mark(X), X, mark(X))
cActive → a
cActive → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(f(x1, x2, x3)) → MARK(x3)
MARK(f(x1, x2, x3)) → FACTIVE(mark(x1), x2, mark(x3))
FACTIVE(a, b, X) → FACTIVE(mark(X), X, mark(X))
MARK(f(x1, x2, x3)) → MARK(x1)
FACTIVE(a, b, X) → MARK(X)
MARK(c) → CACTIVE

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(mark(x1), x2, mark(x3))
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(c) → cActive
cActive → c
mark(a) → a
mark(b) → b
fActive(a, b, X) → fActive(mark(X), X, mark(X))
cActive → a
cActive → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(f(x1, x2, x3)) → MARK(x3)
MARK(f(x1, x2, x3)) → FACTIVE(mark(x1), x2, mark(x3))
FACTIVE(a, b, X) → FACTIVE(mark(X), X, mark(X))
MARK(f(x1, x2, x3)) → MARK(x1)
FACTIVE(a, b, X) → MARK(X)

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(mark(x1), x2, mark(x3))
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(c) → cActive
cActive → c
mark(a) → a
mark(b) → b
fActive(a, b, X) → fActive(mark(X), X, mark(X))
cActive → a
cActive → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(f(x1, x2, x3)) → FACTIVE(mark(x1), x2, mark(x3)) at position [0] we obtained the following new rules:

MARK(f(a, y1, y2)) → FACTIVE(a, y1, mark(y2))
MARK(f(c, y1, y2)) → FACTIVE(cActive, y1, mark(y2))
MARK(f(f(x0, x1, x2), y1, y2)) → FACTIVE(fActive(mark(x0), x1, mark(x2)), y1, mark(y2))
MARK(f(b, y1, y2)) → FACTIVE(b, y1, mark(y2))

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(f(c, y1, y2)) → FACTIVE(cActive, y1, mark(y2))
MARK(f(a, y1, y2)) → FACTIVE(a, y1, mark(y2))
MARK(f(x1, x2, x3)) → MARK(x3)
MARK(f(f(x0, x1, x2), y1, y2)) → FACTIVE(fActive(mark(x0), x1, mark(x2)), y1, mark(y2))
MARK(f(b, y1, y2)) → FACTIVE(b, y1, mark(y2))
FACTIVE(a, b, X) → FACTIVE(mark(X), X, mark(X))
MARK(f(x1, x2, x3)) → MARK(x1)
FACTIVE(a, b, X) → MARK(X)

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(mark(x1), x2, mark(x3))
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(c) → cActive
cActive → c
mark(a) → a
mark(b) → b
fActive(a, b, X) → fActive(mark(X), X, mark(X))
cActive → a
cActive → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(f(c, y1, y2)) → FACTIVE(cActive, y1, mark(y2))
MARK(f(a, y1, y2)) → FACTIVE(a, y1, mark(y2))
MARK(f(x1, x2, x3)) → MARK(x3)
MARK(f(f(x0, x1, x2), y1, y2)) → FACTIVE(fActive(mark(x0), x1, mark(x2)), y1, mark(y2))
FACTIVE(a, b, X) → FACTIVE(mark(X), X, mark(X))
MARK(f(x1, x2, x3)) → MARK(x1)
FACTIVE(a, b, X) → MARK(X)

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(mark(x1), x2, mark(x3))
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(c) → cActive
cActive → c
mark(a) → a
mark(b) → b
fActive(a, b, X) → fActive(mark(X), X, mark(X))
cActive → a
cActive → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(f(c, y1, y2)) → FACTIVE(cActive, y1, mark(y2)) at position [0] we obtained the following new rules:

MARK(f(c, y0, y1)) → FACTIVE(c, y0, mark(y1))
MARK(f(c, y0, y1)) → FACTIVE(b, y0, mark(y1))
MARK(f(c, y0, y1)) → FACTIVE(a, y0, mark(y1))

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(f(x1, x2, x3)) → MARK(x3)
MARK(f(a, y1, y2)) → FACTIVE(a, y1, mark(y2))
MARK(f(f(x0, x1, x2), y1, y2)) → FACTIVE(fActive(mark(x0), x1, mark(x2)), y1, mark(y2))
MARK(f(c, y0, y1)) → FACTIVE(c, y0, mark(y1))
MARK(f(c, y0, y1)) → FACTIVE(a, y0, mark(y1))
MARK(f(c, y0, y1)) → FACTIVE(b, y0, mark(y1))
FACTIVE(a, b, X) → FACTIVE(mark(X), X, mark(X))
MARK(f(x1, x2, x3)) → MARK(x1)
FACTIVE(a, b, X) → MARK(X)

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(mark(x1), x2, mark(x3))
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(c) → cActive
cActive → c
mark(a) → a
mark(b) → b
fActive(a, b, X) → fActive(mark(X), X, mark(X))
cActive → a
cActive → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ QDP

                              ↳ QDPOrderProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(f(a, y1, y2)) → FACTIVE(a, y1, mark(y2))
MARK(f(x1, x2, x3)) → MARK(x3)
MARK(f(f(x0, x1, x2), y1, y2)) → FACTIVE(fActive(mark(x0), x1, mark(x2)), y1, mark(y2))
MARK(f(c, y0, y1)) → FACTIVE(a, y0, mark(y1))
FACTIVE(a, b, X) → FACTIVE(mark(X), X, mark(X))
MARK(f(x1, x2, x3)) → MARK(x1)
FACTIVE(a, b, X) → MARK(X)

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(mark(x1), x2, mark(x3))
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(c) → cActive
cActive → c
mark(a) → a
mark(b) → b
fActive(a, b, X) → fActive(mark(X), X, mark(X))
cActive → a
cActive → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(f(f(x0, x1, x2), y1, y2)) → FACTIVE(fActive(mark(x0), x1, mark(x2)), y1, mark(y2))

The remaining pairs can at least be oriented weakly.

MARK(f(a, y1, y2)) → FACTIVE(a, y1, mark(y2))
MARK(f(x1, x2, x3)) → MARK(x3)
MARK(f(c, y0, y1)) → FACTIVE(a, y0, mark(y1))
FACTIVE(a, b, X) → FACTIVE(mark(X), X, mark(X))
MARK(f(x1, x2, x3)) → MARK(x1)
FACTIVE(a, b, X) → MARK(X)

Used ordering: Polynomial interpretation [25]:

POL(FACTIVE(x₁, x₂, x₃)) = x₁
POL(MARK(x₁)) = 1
POL(a) = 1
POL(b) = 0
POL(c) = 0
POL(cActive) = 1
POL(f(x₁, x₂, x₃)) = 0
POL(fActive(x₁, x₂, x₃)) = 0
POL(mark(x₁)) = 1

The following usable rules [17] were oriented:

mark(f(x1, x2, x3)) → fActive(mark(x1), x2, mark(x3))
fActive(x1, x2, x3) → f(x1, x2, x3)
fActive(a, b, X) → fActive(mark(X), X, mark(X))
cActive → a
cActive → b
mark(c) → cActive
cActive → c
mark(a) → a
mark(b) → b

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ QDP

                              ↳ QDPOrderProof

                                ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(f(x1, x2, x3)) → MARK(x3)
MARK(f(a, y1, y2)) → FACTIVE(a, y1, mark(y2))
MARK(f(c, y0, y1)) → FACTIVE(a, y0, mark(y1))
FACTIVE(a, b, X) → FACTIVE(mark(X), X, mark(X))
MARK(f(x1, x2, x3)) → MARK(x1)
FACTIVE(a, b, X) → MARK(X)

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(mark(x1), x2, mark(x3))
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(c) → cActive
cActive → c
mark(a) → a
mark(b) → b
fActive(a, b, X) → fActive(mark(X), X, mark(X))
cActive → a
cActive → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We applied the Trivial transformation to transform the context-sensitive TRS to a usual TRS.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f(a, b, X) → f(X, X, X)
c → a
c → b

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

F(a, b, X) → F(X, X, X)

The TRS R consists of the following rules:

f(a, b, X) → f(X, X, X)
c → a
c → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

F(a, b, X) → F(X, X, X)

The TRS R consists of the following rules:

f(a, b, X) → f(X, X, X)
c → a
c → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.